COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x y z v w z1 z2
C00003 ENDMK
C⊗;
declare INDVAR x y z v w z1 z2;
declare PREDCONST R 3 E 3;
axiom foo:
	∀x y.∃z.R(x,y,z)
	∀x y z1 z2.(R(x,y,z1) ∧ R(x,y,z2) ⊃ z1 = z2)
;;